port(charted-space-core): manifold structure from a ChartedSpaceCore

What this ports

Lee, Introduction to Smooth Manifolds, §1, Lemma 1.35 (parts 1–4):
the separation, countability, smoothness and uniqueness properties of the
topology that a chart-family core (ChartedSpaceCore) generates on its
underlying set.

Index wiring:

• OpenGALib/Manifold.lean — added import OpenGALib.Manifold.Charts.ChartedSpaceCore
  (alphabetical, single-line change).
• OpenGALib.lean (root index) — unchanged; already imports OpenGALib.Manifold.

Core objects / results

The ticket lists no core_objects (all four declarations are theorems):

• Manifold.toTopologicalSpace_t2Space — Lemma 1.35 (2): the generated topology
  is Hausdorff when distinct points are separated by a common chart or by
  disjoint chart domains.
• Manifold.toTopologicalSpace_secondCountableTopology — Lemma 1.35 (3): the
  generated topology is second-countable when a countable subatlas covers the space.
• Manifold.toChartedSpace_isManifold — Lemma 1.35 (4): smooth coordinate changes
  make the generated charted space a smooth manifold.
• Manifold.eq_toTopologicalSpace_of_chartedSpace — Lemma 1.35 (1): the generated
  topology is the unique one realizing the chart family as a charted space.

Design-neutral statement

• Stated directly on Mathlib typeclasses: TopologicalSpace, T2Space,
  SecondCountableTopology, ChartedSpace, IsManifold, ModelWithCorners,
  and Mathlib's ChartedSpaceCore structure. No OpenGA SmoothManifold
  packaging class and no Lee TopologicalManifold were introduced or relied on.
• No transforms in the ticket; in particular no restate was required (the
  source already binds the four Mathlib classes individually, not via
  TopologicalManifold).
• The proofs are carried over verbatim from the source; only the surrounding
  namespace changed (see Deviations).

Deviations from a literal copy

• Renamespacing (RUNBOOK §1, design-neutral). The source declares the four
  theorems under namespace ChartedSpaceCore, which is not on the project
  namespace whitelist (OpenGALib, Manifold, Riemannian,
  GeometricMeasureTheory, OpenPartialHomeomorph). Per the namespace policy,
  the declarations were moved into namespace Manifold with their names
  unchanged (toTopologicalSpace_t2Space, etc.). This is a pure namespace
  move, not a rename-to-dodge-the-gate; the Mathlib type ChartedSpaceCore
  itself is untouched and still referenced by its full name inside the proofs
  (e.g. ChartedSpaceCore.toTopologicalSpace).
• Dropped the source's pipeline scaffolding comments (-- Declarations ... appended below, lean_leansearch note) and the bare namespace ChartedSpaceCore wrapper. Added the module docstring (NAMING_CONVENTION
  template + provenance line) and **Math.** / **Eng.** per-declaration
  docstrings required by the docstring gate.
• No inlined dependencies, no Mathlib API renames.

Provenance

import/smooth-manifolds-lee @ a5f308c:

• staging/SmoothManifoldsLee/SmoothManifoldsLee/Chap01/Sec01_04/Lemma_1_35.lean

Gate results (local, full run — all six green)

✓ build           build 通过
✓ no-sorry        改动文件无 sorry
✓ namespace       顶层 namespace 均在白名单内
✓ provenance      出处行齐全
✓ docstring       双 docstring 齐全
✓ linter-baseline 占位通过：自定义 linter 尚未接入（issue #61 待决）

Report: projects/sml-to-openga/ledger/reports/ticket03-20260614T043136Z.json

Review focus (minimal trusted base)

Proofs are kernel-checked. Reviewer need only confirm the statements name
the same mathematical objects as Lee's Lemma 1.35 (1)–(4) — i.e. that the four
theorem signatures (separation hypothesis ⇒ Hausdorff; countable cover ⇒
second-countable; smooth transitions ⇒ IsManifold; charted-space compatibility
⇒ topology uniqueness) faithfully transcribe the source statements after the
ChartedSpaceCore → Manifold namespace move.

Stacking note

Branch port/charted-space-core is cut from the stacked batch tip
port/precompact-basis (not directly from origin/develop). Ticket #3 has no
declared deps; the new module is an independent unit (it does not import the
coordinate-ball or precompact-basis modules).